R:Realizer, i:Id. R-Feasible(R)  R-init(R;i)  x:Id fp DeclaredType(R-ds(R;i);x) 

latex

Definitions

t  T, x:AB(x), x:A. B(x), P  Q, Type, f || g, IdDeq, x.A(x), x. t(x), f  g, f  g, Void, {x:A| B(x) }, (x  l), type List, R-init(R;i), A || B, R-Feasible(R), x:AB(x), Prop, P & Q, AtomFree(T;x), , s = t, b, A, b, , x:A. B(x), Top, x : v, a = b, P  Q, Unit, left+right, if b t else f fi, True, f(a), x:A. B(x), Dec(P), State(ds), x  dom(f), x,y. t(x;y), xdom(f). v=f(x)   P(x;v), source(l), lnk(k), destination(l), tag(k), f(x)?z, IdLnk, isrcv(k), es realizer ind Rrframe compseq tag def, es realizer ind Rbframe compseq tag def, es realizer ind Raframe compseq tag def, es realizer ind Rpre compseq tag def, es realizer ind Rsends compseq tag def, es realizer ind Reffect compseq tag def, es realizer ind Rsframe compseq tag def, es realizer ind Rframe compseq tag def, es realizer ind Rinit compseq tag def, es realizer ind Rplus compseq tag def, es realizer ind Rnone compseq tag def, Knd, rec(x.A(x)), Realizer, R-ds(R;i), DeclaredType(ds;x), Id, a:A fp B(a)

Lemmas

es realizer wf, unit wf, Knd wf, isrcv wf, IdLnk wf, fpf-cap wf, tagof wf, ldst wf, lnk wf, lsrc wf, ifthenelse wf, fpf wf, fpf-all wf, fpf-dom wf, decl-state wf, decidable wf, fpf-trivial-subtype-top, true wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert-eq-id, eq id wf, fpf-single wf, fpf-cap-single1, bool wf, bnot wf, not wf, assert wf, fpf-empty wf, atom-free wf, R-Feasible wf, R-compat wf, subtype rel product, subtype rel dep function, decl-type wf, subtype rel self, l member wf, subtype-fpf-cap-void, fpf-join wf, fpf-sub-join-left, fpf-sub-join-right, Id wf, id-deq wf, R-ds wf, R-compat-ds